COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	properties of allp
C00006 ENDMK
C⊗;
;properties of allp
(wipe-out)
(get-proofs lispax prf ekl sys)

(proof allp)
;the following formulation of the definition of allp is more convenient when
;deriving instead of rewriting

;1
(axiom |∀phi x u.allp(phi,x.u)⊃phi(x)∧allp(phi,u)|)
(label allpfact)

;2
(axiom |∀phi1 u.(∀y.member(y,u)⊃phi1(y))⊃allp(phi1,u)|)
(label allp_introduction)

;3
(axiom |∀phi1 x u.member(x,u)∧allp(phi1,u)⊃phi1(x)|)
(label allp_elimination)

;4
(axiom |∀u a a1.allp(a,u)∧(∀x.a(x)⊃a1(x))⊃allp(a1,u)|)
(label allp_implication)

;5
(axiom |∀phi1 u.somep(phi1,u)≡(∃x.member(x,u)∧phi1(x))|)
(label somepfact)
(save-proofs allp)